Introduce the annihilator ideal sheaf of a sheaf of modules over a general
site, formulated in the language of (pre)sheaves of modules.

- `PresheafOfModules.SubmoduleSystem`: a restriction-stable family of submodules
  of a presheaf of modules, cutting out a subobject (`toPresheafOfModules`) with
  its inclusion monomorphism (`ι`).
- `PresheafOfModules.annihilatorIdeal`/`annihilator`: the local annihilator
  (sections of `R` whose every restriction annihilates `M`), a subobject of the
  unit, with `mem_annihilatorIdeal` and the contravariance lemma
  `annihilatorIdeal_le_of_surjective`.
- `SheafOfModules.annihilator`: the annihilator as a sheaf of modules, together
  with its monomorphism into `unit R`. The sheaf condition is proved by the
  covering-closure argument for the underlying subpresheaf of the sheaf `R`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>